Inference at * 1 
Iof proof for Lemma assert of bor:



1. p : 
2. q : 
  ((p q))  ((p)  (q)) 

latex

 by ((((OnHyps [2;1] BoolInd) 
CollapseTHEN (Rewrite 
C(UnfoldC `bor` 

C(UnORTHENC HigherC ifthenelse_evalC 
C(ORTHENC HigherC assert_evalC) 
C0))) 
CollapseTHEN (
C(Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n)) (first_tok :t) inil_term))) 

latex

C1: 

C1: 1. True
C1:   True  True
C2: 

C2: 1. True
C2:   False  True
C3: 

C3: 1. True
C3:   True  False
C4: 

C4: 1. False  False
C4:   False
C.

Definitions	ff, , P  Q, P  Q, P  Q, True, if b then t else f fi , tt, t  T, P  Q, p q, b, P  Q, False, Unit, ,
Lemmas	false wf, true wf